DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2024.39

What Monads Can and Cannot Do with a Bit of Extra Time

Authors: Rasmus Ejlers Møgelberg and Maaike Annebet Zwart

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.

Cite as

Rasmus Ejlers Møgelberg and Maaike Annebet Zwart. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{mgelberg_et_al:LIPIcs.CSL.2024.39,
  author =	{M{\o}gelberg, Rasmus Ejlers and Zwart, Maaike Annebet},
  title =	{{What Monads Can and Cannot Do with a Bit of Extra Time}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{39:1--39:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.39},
  URN =		{urn:nbn:de:0030-drops-196823},
  doi =		{10.4230/LIPIcs.CSL.2024.39},
  annote =	{Keywords: Delay Monad, Monad Compositions, Distributive Laws, Guarded Recursion, Type Theory}
}

Search Results

Documents authored by Zwart, Maaike Annebet

What Monads Can and Cannot Do with a Bit of Extra Time

Abstract

Cite as

Thanks for your feedback!

Could not send message